\section{Example System}\label{sec:example-system}
The Muen project contains an example system that makes use of all the
mechanisms described in the previous sections. Figure \ref{fig:example-system}
shows a schematic overview of the system.

\begin{figure}[h]
	\centering
	\input{graph_arch_example}
	\caption{Example system}
	\label{fig:example-system}
\end{figure}

The system is composed of the Muen kernel and four subjects, three of which are
trusted and one xv6 subject is untrusted. The trusted subjects run in the native
profile and are implemented in Ada/SPARK, the untrusted xv6 subject runs a
teaching OS written in C inside the VM profile.

The example system is meant to serve as demonstrator for a real-world use-case:
an untrusted operating system is separated by the Muen kernel and accesses
native, trusted services with a very small TCB. The trusted encrypter service is
implemented completely in SPARK and proven to be free from runtime errors.

The following section explains the different subjects composing the example
system, while section \ref{subsec:keyboard-handling} describes the keyboard
handling in detail to illustrate how the different mechanisms are tied
together.

\subsection{Subjects}

\subsubsection{VT}\label{subsubsec:subject-vt}
The VT subject manages virtual terminal consoles and owns the keyboard. The
system policy therefore assigns the hardware devices shown by listing
\ref{lst:hardware-devs} to the subject. This allows the VT subject to control
the VGA cursor and the contents of the VGA memory. The kernel programs the
system I/O APIC to deliver keyboard interrupts (IRQ 1) to the VT subject.

\begin{lstlisting}[
	language=xml,
	label=lst:hardware-devs,
	caption=Subject device assignment]
<device name="keyboard" irq="1">
    <io_port start="0060" end="0060"/>
    <io_port start="0064" end="0064"/>
</device>

<device name="vga">
    <memory_layout>
        <memory_region physical_address="b8000" virtual_address="b8000" ...
    </memory_layout>
</device>

<device name="cursor">
    <io_port start="03d4" end="03d5"/>
</device>
\end{lstlisting}

The other subjects of the example system have no direct access to the real VGA
memory but write to a distinct page mapped to their (virtual) VGA memory
address (\texttt{0xb8000}). The subject virtual terminal pages are also mapped
into the address space of the VT subject.

If the user hits one of the special keys F1 to F6, the VT subject updates the
VGA memory with the contents of the active session slot's virtual terminal page.
All other keyboard scancodes are copied to a driver page shared with the
untrusted xv6 subject. An event is triggered to inform the virtual keyboard
driver that keyboard data awaits processing.

\subsubsection{Crypter}
The crypter subject uses the libsparkcrypto \cite{libsparkcrypto} library to
provide trusted cryptographic services to clients. On startup, the subject
enters the halted state until it receives an interrupt event indicating a
pending request.

The interrupt resumes the subject and data contained in the subject's request
page is copied for further processing. Currently, the crypter subject creates a
HMAC-SHA-256 message digest over the received data and then copies the hash to
the service response page. An interrupt event is triggered to signal service
completion.

\subsubsection{xv6}\label{subsubsec:xv6}
Xv6\index{xv6} is a Version 6 Unix \cite{wiki:unix6} teaching operating system
developed at MIT \cite{xv6}. While being simple, it implements many key
concepts found in common operating systems, making it an ideal initial target
for the VM profile. Xv6 is written in ANSI C.

Minimal changes to the xv6 source code and a small subject monitor were
required to run it as VM subject on the Muen kernel:
\begin{itemize}
	\item Disable MP support
	\item Ignore disallowed I/O operations (handled by the SM subject)
\end{itemize}

Since the xv6 subject has no direct access to the keyboard, a simple virtual
keyboard driver has been implemented.

\subsubsection{Subject Monitor}
The subject monitor (SM\index{SM}) subject is used to monitor the untrusted xv6
subject. It displays information about I/O operations and has complete access to
the architectural state of the xv6 subject. Currently, no emulation is needed to
run xv6. If an unexpected trap occurs, a state dump is written to the SM's
virtual terminal and further execution is suspended.

\subsection{Keyboard Handling}\label{subsec:keyboard-handling}
This section describes how the keyboard is handled in the example system using
the mechanisms provided by the Muen kernel.

\begin{lstlisting}[
	language=Ada,
	label=lst:ex-irq-routing,
	caption=Example system IRQ routing table]
IRQ_Routing : constant IRQ_Routing_Array := IRQ_Routing_Array'(
  1 => IRQ_Route_Type'(
    CPU    => 0,
    IRQ    => 1,
    Vector => 33));
\end{lstlisting}

When pressing a key on the keyboard, the keyboard controller raises an interrupt
request (IRQ\index{IRQ}) with number 1 to signal new data. The system policy
applied by the Muen kernel on startup enforces that this interrupt is routed to
the appropriate processor running the VT subject. This is done using the IRQ
routing specification generated during policy compilation and depends on the
assignment of hardware devices to subjects. In this case, the keyboard is
assigned to subject 1, which is the VT subject. Listing \ref{lst:ex-irq-routing}
shows the generated IRQ routing table of the example system.

The routing table contains one entry which routes the keyboard IRQ 1 to the CPU
with APIC ID 0. Furthermore, the IRQ is remapped to the interrupt vector 33 so
that on each key press, an interrupt with vector 33 is delivered to CPU0 via its
LAPIC.

The Muen kernel running on CPU0 handles the received interrupt in its
\texttt{Handle\_Irq} procedure. It uses the vector routing table contained in
the interrupt specification compiled by the \texttt{skpolicy} tool, see listing
\ref{lst:ex-vector-routing}. The table instructs the kernel to inject interrupt
vector 33 into the subject with ID 1 by using the interrupt injection mechanism
described in section \ref{subsec:int-injection}.

\begin{lstlisting}[
	language=Ada,
	label=lst:ex-vector-routing,
	caption=Example system CPU0 vector routing table]
Vector_Routing : constant Vector_Routing_Array := Vector_Routing_Array'(
  33     => 1,
  others => Skp.Invalid_Subject);
\end{lstlisting}

The VT subject receives interrupt vector 33 via its interrupt handling routine
and, because it is allowed to access the respective I/O ports, reads in the
keyboard scancodes. If the received scancode is not related to the special keys
F1 to F6 and the currently visible subject is xv6, the scancode data is copied
into a memory page shared with the xv6 subject. The VT subject then triggers an
event to inform the xv6 subject about new data to process. This is done using
the Muen event mechanism.

The kernel running the VT subject forwards the interrupt event to the respective
subject as defined by the policy. In this case, it is the xv6 subject.

The xv6 subject's interrupt handler code detects that a keyboard interrupt has
occurred. The appropriate keyboard handling code is called, which has been
changed to read keyboard scancodes from a shared memory page instead of doing
port I/O. The copied scancode data is then used to drive the terminal console.
